PRISM
=====
Version: 4.5.dev
Date: Sat Apr 03 02:59:17 CEST 2021
Hostname: christopher
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 rabin.100.prism rabin.100.props --property live
Parsing model file "rabin.100.prism"...
Type: MDP
Modules: process1 process2 process3 process4 process5 process6 process7 process8 process9 process10 process11 process12 process13 process14 process15 process16 process17 process18 process19 process20 process21 process22 process23 process24 process25 process26 process27 process28 process29 process30 process31 process32 process33 process34 process35 process36 process37 process38 process39 process40 process41 process42 process43 process44 process45 process46 process47 process48 process49 process50 process51 process52 process53 process54 process55 process56 process57 process58 process59 process60 process61 process62 process63 process64 process65 process66 process67 process68 process69 process70 process71 process72 process73 process74 process75 process76 process77 process78 process79 process80 process81 process82 process83 process84 process85 process86 process87 process88 process89 process90 process91 process92 process93 process94 process95 process96 process97 process98 process99 process100
Variables: c b r p1 b1 r1 draw1 p2 b2 r2 draw2 p3 b3 r3 draw3 p4 b4 r4 draw4 p5 b5 r5 draw5 p6 b6 r6 draw6 p7 b7 r7 draw7 p8 b8 r8 draw8 p9 b9 r9 draw9 p10 b10 r10 draw10 p11 b11 r11 draw11 p12 b12 r12 draw12 p13 b13 r13 draw13 p14 b14 r14 draw14 p15 b15 r15 draw15 p16 b16 r16 draw16 p17 b17 r17 draw17 p18 b18 r18 draw18 p19 b19 r19 draw19 p20 b20 r20 draw20 p21 b21 r21 draw21 p22 b22 r22 draw22 p23 b23 r23 draw23 p24 b24 r24 draw24 p25 b25 r25 draw25 p26 b26 r26 draw26 p27 b27 r27 draw27 p28 b28 r28 draw28 p29 b29 r29 draw29 p30 b30 r30 draw30 p31 b31 r31 draw31 p32 b32 r32 draw32 p33 b33 r33 draw33 p34 b34 r34 draw34 p35 b35 r35 draw35 p36 b36 r36 draw36 p37 b37 r37 draw37 p38 b38 r38 draw38 p39 b39 r39 draw39 p40 b40 r40 draw40 p41 b41 r41 draw41 p42 b42 r42 draw42 p43 b43 r43 draw43 p44 b44 r44 draw44 p45 b45 r45 draw45 p46 b46 r46 draw46 p47 b47 r47 draw47 p48 b48 r48 draw48 p49 b49 r49 draw49 p50 b50 r50 draw50 p51 b51 r51 draw51 p52 b52 r52 draw52 p53 b53 r53 draw53 p54 b54 r54 draw54 p55 b55 r55 draw55 p56 b56 r56 draw56 p57 b57 r57 draw57 p58 b58 r58 draw58 p59 b59 r59 draw59 p60 b60 r60 draw60 p61 b61 r61 draw61 p62 b62 r62 draw62 p63 b63 r63 draw63 p64 b64 r64 draw64 p65 b65 r65 draw65 p66 b66 r66 draw66 p67 b67 r67 draw67 p68 b68 r68 draw68 p69 b69 r69 draw69 p70 b70 r70 draw70 p71 b71 r71 draw71 p72 b72 r72 draw72 p73 b73 r73 draw73 p74 b74 r74 draw74 p75 b75 r75 draw75 p76 b76 r76 draw76 p77 b77 r77 draw77 p78 b78 r78 draw78 p79 b79 r79 draw79 p80 b80 r80 draw80 p81 b81 r81 draw81 p82 b82 r82 draw82 p83 b83 r83 draw83 p84 b84 r84 draw84 p85 b85 r85 draw85 p86 b86 r86 draw86 p87 b87 r87 draw87 p88 b88 r88 draw88 p89 b89 r89 draw89 p90 b90 r90 draw90 p91 b91 r91 draw91 p92 b92 r92 draw92 p93 b93 r93 draw93 p94 b94 r94 draw94 p95 b95 r95 draw95 p96 b96 r96 draw96 p97 b97 r97 draw97 p98 b98 r98 draw98 p99 b99 r99 draw99 p100 b100 r100 draw100
Parsing properties file "rabin.100.props"...
1 property:
(1) "live": Pmax=? [ F (p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2|p11=2|p12=2|p13=2|p14=2|p15=2|p16=2|p17=2|p18=2|p19=2|p20=2|p21=2|p22=2|p23=2|p24=2|p25=2|p26=2|p27=2|p28=2|p29=2|p30=2|p31=2|p32=2|p33=2|p34=2|p35=2|p36=2|p37=2|p38=2|p39=2|p40=2|p41=2|p42=2|p43=2|p44=2|p45=2|p46=2|p47=2|p48=2|p49=2|p50=2|p51=2|p52=2|p53=2|p54=2|p55=2|p56=2|p57=2|p58=2|p59=2|p60=2|p61=2|p62=2|p63=2|p64=2|p65=2|p66=2|p67=2|p68=2|p69=2|p70=2|p71=2|p72=2|p73=2|p74=2|p75=2|p76=2|p77=2|p78=2|p79=2|p80=2|p81=2|p82=2|p83=2|p84=2|p85=2|p86=2|p87=2|p88=2|p89=2|p90=2|p91=2|p92=2|p93=2|p94=2|p95=2|p96=2|p97=2|p98=2|p99=2|p100=2) ]
---------------------------------------------------------------------
Model checking: "live": Pmax=? [ F (p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2|p11=2|p12=2|p13=2|p14=2|p15=2|p16=2|p17=2|p18=2|p19=2|p20=2|p21=2|p22=2|p23=2|p24=2|p25=2|p26=2|p27=2|p28=2|p29=2|p30=2|p31=2|p32=2|p33=2|p34=2|p35=2|p36=2|p37=2|p38=2|p39=2|p40=2|p41=2|p42=2|p43=2|p44=2|p45=2|p46=2|p47=2|p48=2|p49=2|p50=2|p51=2|p52=2|p53=2|p54=2|p55=2|p56=2|p57=2|p58=2|p59=2|p60=2|p61=2|p62=2|p63=2|p64=2|p65=2|p66=2|p67=2|p68=2|p69=2|p70=2|p71=2|p72=2|p73=2|p74=2|p75=2|p76=2|p77=2|p78=2|p79=2|p80=2|p81=2|p82=2|p83=2|p84=2|p85=2|p86=2|p87=2|p88=2|p89=2|p90=2|p91=2|p92=2|p93=2|p94=2|p95=2|p96=2|p97=2|p98=2|p99=2|p100=2) ]
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
#
# A fatal error has been detected by the Java Runtime Environment:
#
# SIGSEGV (0xb) at pc=0x00007f0864101b98, pid=556122, tid=556130
#
# JRE version: OpenJDK Runtime Environment (13.0.2+8) (build 13.0.2+8)
# Java VM: OpenJDK 64-Bit Server VM (13.0.2+8, mixed mode, sharing, tiered, compressed oops, g1 gc, linux-amd64)
# Problematic frame:
# C [libdd.so+0x2fb98] Cudd_Ref+0x8
#
# Core dump will be written. Default location: Core dumps may be processed with "/usr/share/apport/apport %p %s %c %d %P %E" (or dumping to /home/michaela/qcomp2020/core.556122)
#
# An error report file with more information is saved as:
# /home/michaela/qcomp2020/hs_err_pid556122.log
#
# If you would like to submit a bug report, please visit:
# http://bugreport.java.com/bugreport/crash.jsp
# The crash happened outside the Java Virtual Machine in native code.
# See problematic frame for where to report the bug.
#